0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 1426 ms)
↳10 BOUNDS(1, n^2)
app(x, y) → helpa(0, plus(length(x), length(y)), x, y)
plus(x, 0) → x
plus(x, s(y)) → s(plus(x, y))
length(nil) → 0
length(cons(x, y)) → s(length(y))
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if(true, c, l, ys, zs) → nil
if(false, c, l, ys, zs) → helpb(c, l, ys, zs)
take(0, cons(x, xs), ys) → x
take(0, nil, cons(y, ys)) → y
take(s(c), cons(x, xs), ys) → take(c, xs, ys)
take(s(c), nil, cons(y, ys)) → take(c, nil, ys)
helpb(c, l, ys, zs) → cons(take(c, ys, zs), helpa(s(c), l, ys, zs))
app(x, y) → helpa(0, plus(length(x), length(y)), x, y) [1]
plus(x, 0) → x [1]
plus(x, s(y)) → s(plus(x, y)) [1]
length(nil) → 0 [1]
length(cons(x, y)) → s(length(y)) [1]
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs) [1]
ge(x, 0) → true [1]
ge(0, s(x)) → false [1]
ge(s(x), s(y)) → ge(x, y) [1]
if(true, c, l, ys, zs) → nil [1]
if(false, c, l, ys, zs) → helpb(c, l, ys, zs) [1]
take(0, cons(x, xs), ys) → x [1]
take(0, nil, cons(y, ys)) → y [1]
take(s(c), cons(x, xs), ys) → take(c, xs, ys) [1]
take(s(c), nil, cons(y, ys)) → take(c, nil, ys) [1]
helpb(c, l, ys, zs) → cons(take(c, ys, zs), helpa(s(c), l, ys, zs)) [1]
app(x, y) → helpa(0, plus(length(x), length(y)), x, y) [1]
plus(x, 0) → x [1]
plus(x, s(y)) → s(plus(x, y)) [1]
length(nil) → 0 [1]
length(cons(x, y)) → s(length(y)) [1]
helpa(c, l, ys, zs) → if(ge(c, l), c, l, ys, zs) [1]
ge(x, 0) → true [1]
ge(0, s(x)) → false [1]
ge(s(x), s(y)) → ge(x, y) [1]
if(true, c, l, ys, zs) → nil [1]
if(false, c, l, ys, zs) → helpb(c, l, ys, zs) [1]
take(0, cons(x, xs), ys) → x [1]
take(0, nil, cons(y, ys)) → y [1]
take(s(c), cons(x, xs), ys) → take(c, xs, ys) [1]
take(s(c), nil, cons(y, ys)) → take(c, nil, ys) [1]
helpb(c, l, ys, zs) → cons(take(c, ys, zs), helpa(s(c), l, ys, zs)) [1]
| app :: nil:cons:xs → nil:cons:xs → nil:cons:xs helpa :: 0:s → 0:s → nil:cons:xs → nil:cons:xs → nil:cons:xs 0 :: 0:s plus :: 0:s → 0:s → 0:s length :: nil:cons:xs → 0:s s :: 0:s → 0:s nil :: nil:cons:xs cons :: take → nil:cons:xs → nil:cons:xs if :: true:false → 0:s → 0:s → nil:cons:xs → nil:cons:xs → nil:cons:xs ge :: 0:s → 0:s → true:false true :: true:false false :: true:false helpb :: 0:s → 0:s → nil:cons:xs → nil:cons:xs → nil:cons:xs take :: 0:s → nil:cons:xs → nil:cons:xs → take xs :: nil:cons:xs |
length(v0) → null_length [0]
take(v0, v1, v2) → null_take [0]
plus(v0, v1) → null_plus [0]
ge(v0, v1) → null_ge [0]
if(v0, v1, v2, v3, v4) → null_if [0]
null_length, null_take, null_plus, null_ge, null_if
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
nil => 0
true => 2
false => 1
xs => 1
null_length => 0
null_take => 0
null_plus => 0
null_ge => 0
null_if => 0
app(z, z') -{ 1 }→ helpa(0, plus(length(x), length(y)), x, y) :|: x >= 0, y >= 0, z = x, z' = y
ge(z, z') -{ 1 }→ ge(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
ge(z, z') -{ 1 }→ 2 :|: x >= 0, z = x, z' = 0
ge(z, z') -{ 1 }→ 1 :|: z' = 1 + x, x >= 0, z = 0
ge(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
helpa(z, z', z'', z1) -{ 1 }→ if(ge(c, l), c, l, ys, zs) :|: z' = l, c >= 0, ys >= 0, zs >= 0, z'' = ys, z = c, l >= 0, z1 = zs
helpb(z, z', z'', z1) -{ 1 }→ 1 + take(c, ys, zs) + helpa(1 + c, l, ys, zs) :|: z' = l, c >= 0, ys >= 0, zs >= 0, z'' = ys, z = c, l >= 0, z1 = zs
if(z, z', z'', z1, z2) -{ 1 }→ helpb(c, l, ys, zs) :|: z2 = zs, c >= 0, z = 1, ys >= 0, zs >= 0, l >= 0, z' = c, z'' = l, z1 = ys
if(z, z', z'', z1, z2) -{ 1 }→ 0 :|: z = 2, z2 = zs, c >= 0, ys >= 0, zs >= 0, l >= 0, z' = c, z'' = l, z1 = ys
if(z, z', z'', z1, z2) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, v4 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, z2 = v4, v2 >= 0, v3 >= 0
length(z) -{ 1 }→ 0 :|: z = 0
length(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
length(z) -{ 1 }→ 1 + length(y) :|: z = 1 + x + y, x >= 0, y >= 0
plus(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
plus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
plus(z, z') -{ 1 }→ 1 + plus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = x
take(z, z', z'') -{ 1 }→ x :|: ys >= 0, x >= 0, z'' = ys, z = 0, z' = 1 + x + 1
take(z, z', z'') -{ 1 }→ y :|: z'' = 1 + y + ys, ys >= 0, y >= 0, z = 0, z' = 0
take(z, z', z'') -{ 1 }→ take(c, 1, ys) :|: c >= 0, ys >= 0, x >= 0, z'' = ys, z = 1 + c, z' = 1 + x + 1
take(z, z', z'') -{ 1 }→ take(c, 0, ys) :|: z'' = 1 + y + ys, c >= 0, ys >= 0, y >= 0, z = 1 + c, z' = 0
take(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
| eq(start(V, V1, V9, V10, V19),0,[app(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9, V10, V19),0,[plus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9, V10, V19),0,[length(V, Out)],[V >= 0]). eq(start(V, V1, V9, V10, V19),0,[helpa(V, V1, V9, V10, Out)],[V >= 0,V1 >= 0,V9 >= 0,V10 >= 0]). eq(start(V, V1, V9, V10, V19),0,[ge(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V9, V10, V19),0,[if(V, V1, V9, V10, V19, Out)],[V >= 0,V1 >= 0,V9 >= 0,V10 >= 0,V19 >= 0]). eq(start(V, V1, V9, V10, V19),0,[take(V, V1, V9, Out)],[V >= 0,V1 >= 0,V9 >= 0]). eq(start(V, V1, V9, V10, V19),0,[helpb(V, V1, V9, V10, Out)],[V >= 0,V1 >= 0,V9 >= 0,V10 >= 0]). eq(app(V, V1, Out),1,[length(V2, Ret10),length(V3, Ret11),plus(Ret10, Ret11, Ret1),helpa(0, Ret1, V2, V3, Ret)],[Out = Ret,V2 >= 0,V3 >= 0,V = V2,V1 = V3]). eq(plus(V, V1, Out),1,[],[Out = V4,V4 >= 0,V = V4,V1 = 0]). eq(plus(V, V1, Out),1,[plus(V5, V6, Ret12)],[Out = 1 + Ret12,V1 = 1 + V6,V5 >= 0,V6 >= 0,V = V5]). eq(length(V, Out),1,[],[Out = 0,V = 0]). eq(length(V, Out),1,[length(V7, Ret13)],[Out = 1 + Ret13,V = 1 + V7 + V8,V8 >= 0,V7 >= 0]). eq(helpa(V, V1, V9, V10, Out),1,[ge(V11, V12, Ret0),if(Ret0, V11, V12, V13, V14, Ret2)],[Out = Ret2,V1 = V12,V11 >= 0,V13 >= 0,V14 >= 0,V9 = V13,V = V11,V12 >= 0,V10 = V14]). eq(ge(V, V1, Out),1,[],[Out = 2,V15 >= 0,V = V15,V1 = 0]). eq(ge(V, V1, Out),1,[],[Out = 1,V1 = 1 + V16,V16 >= 0,V = 0]). eq(ge(V, V1, Out),1,[ge(V17, V18, Ret3)],[Out = Ret3,V1 = 1 + V18,V17 >= 0,V18 >= 0,V = 1 + V17]). eq(if(V, V1, V9, V10, V19, Out),1,[],[Out = 0,V = 2,V19 = V20,V21 >= 0,V22 >= 0,V20 >= 0,V23 >= 0,V1 = V21,V9 = V23,V10 = V22]). eq(if(V, V1, V9, V10, V19, Out),1,[helpb(V24, V25, V26, V27, Ret4)],[Out = Ret4,V19 = V27,V24 >= 0,V = 1,V26 >= 0,V27 >= 0,V25 >= 0,V1 = V24,V9 = V25,V10 = V26]). eq(take(V, V1, V9, Out),1,[],[Out = V28,V29 >= 0,V28 >= 0,V9 = V29,V = 0,V1 = 2 + V28]). eq(take(V, V1, V9, Out),1,[],[Out = V30,V9 = 1 + V30 + V31,V31 >= 0,V30 >= 0,V = 0,V1 = 0]). eq(take(V, V1, V9, Out),1,[take(V32, 1, V33, Ret5)],[Out = Ret5,V32 >= 0,V33 >= 0,V34 >= 0,V9 = V33,V = 1 + V32,V1 = 2 + V34]). eq(take(V, V1, V9, Out),1,[take(V35, 0, V36, Ret6)],[Out = Ret6,V9 = 1 + V36 + V37,V35 >= 0,V36 >= 0,V37 >= 0,V = 1 + V35,V1 = 0]). eq(helpb(V, V1, V9, V10, Out),1,[take(V38, V39, V40, Ret01),helpa(1 + V38, V41, V39, V40, Ret14)],[Out = 1 + Ret01 + Ret14,V1 = V41,V38 >= 0,V39 >= 0,V40 >= 0,V9 = V39,V = V38,V41 >= 0,V10 = V40]). eq(length(V, Out),0,[],[Out = 0,V42 >= 0,V = V42]). eq(take(V, V1, V9, Out),0,[],[Out = 0,V43 >= 0,V9 = V44,V45 >= 0,V = V43,V1 = V45,V44 >= 0]). eq(plus(V, V1, Out),0,[],[Out = 0,V46 >= 0,V47 >= 0,V = V46,V1 = V47]). eq(ge(V, V1, Out),0,[],[Out = 0,V48 >= 0,V49 >= 0,V = V48,V1 = V49]). eq(if(V, V1, V9, V10, V19, Out),0,[],[Out = 0,V10 = V50,V51 >= 0,V52 >= 0,V9 = V53,V54 >= 0,V = V51,V1 = V54,V19 = V52,V53 >= 0,V50 >= 0]). input_output_vars(app(V,V1,Out),[V,V1],[Out]). input_output_vars(plus(V,V1,Out),[V,V1],[Out]). input_output_vars(length(V,Out),[V],[Out]). input_output_vars(helpa(V,V1,V9,V10,Out),[V,V1,V9,V10],[Out]). input_output_vars(ge(V,V1,Out),[V,V1],[Out]). input_output_vars(if(V,V1,V9,V10,V19,Out),[V,V1,V9,V10,V19],[Out]). input_output_vars(take(V,V1,V9,Out),[V,V1,V9],[Out]). input_output_vars(helpb(V,V1,V9,V10,Out),[V,V1,V9,V10],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [ge/3]
1. recursive : [take/4]
2. recursive : [helpa/5,helpb/5,if/6]
3. recursive : [length/2]
4. recursive : [plus/3]
5. non_recursive : [app/3]
6. non_recursive : [start/5]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into ge/3
1. SCC is partially evaluated into take/4
2. SCC is partially evaluated into helpa/5
3. SCC is partially evaluated into length/2
4. SCC is partially evaluated into plus/3
5. SCC is partially evaluated into app/3
6. SCC is partially evaluated into start/5
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations ge/3
* CE 30 is refined into CE [31]
* CE 27 is refined into CE [32]
* CE 28 is refined into CE [33]
* CE 29 is refined into CE [34]
### Cost equations --> "Loop" of ge/3
* CEs [34] --> Loop 20
* CEs [31] --> Loop 21
* CEs [32] --> Loop 22
* CEs [33] --> Loop 23
### Ranking functions of CR ge(V,V1,Out)
* RF of phase [20]: [V,V1]
#### Partial ranking functions of CR ge(V,V1,Out)
* Partial RF of phase [20]:
- RF of loop [20:1]:
V
V1
### Specialization of cost equations take/4
* CE 16 is refined into CE [35]
* CE 12 is refined into CE [36]
* CE 13 is refined into CE [37]
* CE 14 is refined into CE [38]
* CE 15 is refined into CE [39]
### Cost equations --> "Loop" of take/4
* CEs [38] --> Loop 24
* CEs [39] --> Loop 25
* CEs [35] --> Loop 26
* CEs [36] --> Loop 27
* CEs [37] --> Loop 28
### Ranking functions of CR take(V,V1,V9,Out)
* RF of phase [25]: [V,V9]
#### Partial ranking functions of CR take(V,V1,V9,Out)
* Partial RF of phase [25]:
- RF of loop [25:1]:
V
V9
### Specialization of cost equations helpa/5
* CE 19 is refined into CE [40,41,42,43,44]
* CE 17 is refined into CE [45,46,47,48,49]
* CE 18 is refined into CE [50,51]
### Cost equations --> "Loop" of helpa/5
* CEs [46,50] --> Loop 29
* CEs [45,47,48,49,51] --> Loop 30
* CEs [43] --> Loop 31
* CEs [44] --> Loop 32
* CEs [41] --> Loop 33
* CEs [42] --> Loop 34
* CEs [40] --> Loop 35
### Ranking functions of CR helpa(V,V1,V9,V10,Out)
* RF of phase [31,32]: [-V+V1]
#### Partial ranking functions of CR helpa(V,V1,V9,V10,Out)
* Partial RF of phase [31,32]:
- RF of loop [31:1,32:1]:
-V+V1
- RF of loop [32:1]:
-V+V10
### Specialization of cost equations length/2
* CE 24 is refined into CE [52]
* CE 26 is refined into CE [53]
* CE 25 is refined into CE [54]
### Cost equations --> "Loop" of length/2
* CEs [54] --> Loop 36
* CEs [52,53] --> Loop 37
### Ranking functions of CR length(V,Out)
* RF of phase [36]: [V]
#### Partial ranking functions of CR length(V,Out)
* Partial RF of phase [36]:
- RF of loop [36:1]:
V
### Specialization of cost equations plus/3
* CE 23 is refined into CE [55]
* CE 21 is refined into CE [56]
* CE 22 is refined into CE [57]
### Cost equations --> "Loop" of plus/3
* CEs [57] --> Loop 38
* CEs [55] --> Loop 39
* CEs [56] --> Loop 40
### Ranking functions of CR plus(V,V1,Out)
* RF of phase [38]: [V1]
#### Partial ranking functions of CR plus(V,V1,Out)
* Partial RF of phase [38]:
- RF of loop [38:1]:
V1
### Specialization of cost equations app/3
* CE 20 is refined into CE [58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84]
### Cost equations --> "Loop" of app/3
* CEs [71] --> Loop 41
* CEs [77] --> Loop 42
* CEs [62,67,81] --> Loop 43
* CEs [64,69,73,79,83] --> Loop 44
* CEs [72] --> Loop 45
* CEs [63,68,78,82] --> Loop 46
* CEs [58,59,60,65,70,74,75,76,80,84] --> Loop 47
* CEs [61,66] --> Loop 48
### Ranking functions of CR app(V,V1,Out)
#### Partial ranking functions of CR app(V,V1,Out)
### Specialization of cost equations start/5
* CE 3 is refined into CE [85]
* CE 2 is refined into CE [86]
* CE 4 is refined into CE [87,88,89,90,91,92,93,94]
* CE 5 is refined into CE [95,96,97,98,99,100,101,102]
* CE 6 is refined into CE [103,104,105,106,107,108,109,110]
* CE 7 is refined into CE [111,112,113,114]
* CE 8 is refined into CE [115,116]
* CE 9 is refined into CE [117,118,119,120,121,122]
* CE 10 is refined into CE [123,124,125,126,127]
* CE 11 is refined into CE [128,129,130,131]
### Cost equations --> "Loop" of start/5
* CEs [101,102] --> Loop 49
* CEs [85] --> Loop 50
* CEs [93,94] --> Loop 51
* CEs [89,90] --> Loop 52
* CEs [87,88,91,92] --> Loop 53
* CEs [103,118,119,123,129] --> Loop 54
* CEs [97,98,120] --> Loop 55
* CEs [95,96,117] --> Loop 56
* CEs [86,99,100,104,105,106,107,108,109,110,111,112,113,114,115,116,121,122,124,125,126,127,128,130,131] --> Loop 57
### Ranking functions of CR start(V,V1,V9,V10,V19)
#### Partial ranking functions of CR start(V,V1,V9,V10,V19)
Computing Bounds
=====================================
#### Cost of chains of ge(V,V1,Out):
* Chain [[20],23]: 1*it(20)+1
Such that:it(20) =< V
with precondition: [Out=1,V>=1,V1>=V+1]
* Chain [[20],22]: 1*it(20)+1
Such that:it(20) =< V1
with precondition: [Out=2,V1>=1,V>=V1]
* Chain [[20],21]: 1*it(20)+0
Such that:it(20) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [23]: 1
with precondition: [V=0,Out=1,V1>=1]
* Chain [22]: 1
with precondition: [V1=0,Out=2,V>=0]
* Chain [21]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of take(V,V1,V9,Out):
* Chain [[25],28]: 1*it(25)+1
Such that:it(25) =< V
with precondition: [V1=0,V>=1,Out>=0,V9>=Out+V+1]
* Chain [[25],26]: 1*it(25)+0
Such that:it(25) =< V9
with precondition: [V1=0,Out=0,V>=1,V9>=1]
* Chain [28]: 1
with precondition: [V=0,V1=0,Out>=0,V9>=Out+1]
* Chain [27]: 1
with precondition: [V=0,V1=Out+2,V1>=2,V9>=0]
* Chain [26]: 0
with precondition: [Out=0,V>=0,V1>=0,V9>=0]
* Chain [24,26]: 1
with precondition: [Out=0,V>=1,V1>=2,V9>=0]
#### Cost of chains of helpa(V,V1,V9,V10,Out):
* Chain [[31,32],30]: 5*it(31)+5*it(32)+4*s(3)+1*s(15)+1*s(16)+2*s(17)+3
Such that:it(32) =< -V+V10
aux(4) =< V10
aux(8) =< -V+V1
aux(9) =< V1
it(32) =< aux(8)
s(3) =< aux(9)
it(31) =< aux(8)
aux(5) =< aux(9)
s(16) =< it(31)*aux(4)
s(15) =< it(31)*aux(9)
s(18) =< it(32)*aux(5)
s(17) =< s(18)
with precondition: [V>=1,V9>=0,V10>=0,Out>=1,V1>=V+1]
* Chain [35,[31,32],30]: 9*it(31)+5*it(32)+1*s(15)+1*s(16)+2*s(17)+8
Such that:aux(10) =< V1
aux(11) =< V10
it(32) =< aux(11)
it(32) =< aux(10)
it(31) =< aux(10)
aux(5) =< aux(10)
s(16) =< it(31)*aux(11)
s(15) =< it(31)*aux(10)
s(18) =< it(32)*aux(5)
s(17) =< s(18)
with precondition: [V=0,V9=0,V1>=2,V10>=1,Out>=2]
* Chain [35,30]: 3*s(3)+1*s(4)+8
Such that:s(4) =< 1
aux(1) =< V1
s(3) =< aux(1)
with precondition: [V=0,V9=0,V1>=1,Out>=1,V10>=Out]
* Chain [34,[31,32],30]: 9*it(31)+5*it(32)+1*s(15)+1*s(16)+2*s(17)+1*s(19)+8
Such that:aux(12) =< V1
aux(13) =< V10
it(32) =< aux(13)
s(19) =< aux(13)
it(32) =< aux(12)
it(31) =< aux(12)
aux(5) =< aux(12)
s(16) =< it(31)*aux(13)
s(15) =< it(31)*aux(12)
s(18) =< it(32)*aux(5)
s(17) =< s(18)
with precondition: [V=0,V1>=2,V9>=0,V10>=0,Out>=2]
* Chain [34,30]: 3*s(3)+1*s(4)+1*s(19)+8
Such that:s(4) =< 1
aux(1) =< V1
s(19) =< V10
s(3) =< aux(1)
with precondition: [V=0,Out=1,V1>=1,V9>=0,V10>=0]
* Chain [33,[31,32],30]: 9*it(31)+5*it(32)+1*s(15)+1*s(16)+2*s(17)+8
Such that:aux(14) =< V1
aux(15) =< V10
it(32) =< aux(15)
it(32) =< aux(14)
it(31) =< aux(14)
aux(5) =< aux(14)
s(16) =< it(31)*aux(15)
s(15) =< it(31)*aux(14)
s(18) =< it(32)*aux(5)
s(17) =< s(18)
with precondition: [V=0,V1>=2,V9>=2,V10>=0,Out>=V9]
* Chain [33,30]: 3*s(3)+1*s(4)+8
Such that:s(4) =< 1
aux(1) =< V1
s(3) =< aux(1)
with precondition: [V=0,V9=Out+1,V1>=1,V9>=2,V10>=0]
* Chain [30]: 3*s(3)+1*s(4)+3
Such that:s(4) =< V
aux(1) =< V1
s(3) =< aux(1)
with precondition: [Out=0,V>=0,V1>=0,V9>=0,V10>=0]
* Chain [29]: 3
with precondition: [V1=0,Out=0,V>=0,V9>=0,V10>=0]
#### Cost of chains of length(V,Out):
* Chain [[36],37]: 1*it(36)+1
Such that:it(36) =< V
with precondition: [Out>=1,V>=Out]
* Chain [37]: 1
with precondition: [Out=0,V>=0]
#### Cost of chains of plus(V,V1,Out):
* Chain [[38],40]: 1*it(38)+1
Such that:it(38) =< V1
with precondition: [V+V1=Out,V>=0,V1>=1]
* Chain [[38],39]: 1*it(38)+0
Such that:it(38) =< Out
with precondition: [V>=0,Out>=1,V1>=Out]
* Chain [40]: 1
with precondition: [V1=0,V=Out,V>=0]
* Chain [39]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of app(V,V1,Out):
* Chain [48]: 10*s(51)+2*s(53)+12
Such that:aux(20) =< 1
aux(21) =< V1
s(53) =< aux(20)
s(51) =< aux(21)
with precondition: [V=0,Out>=1,V1>=Out]
* Chain [47]: 19*s(67)+8*s(81)+3*s(99)+7
Such that:s(98) =< V+V1
aux(32) =< V
aux(33) =< V1
s(81) =< aux(32)
s(67) =< aux(33)
s(99) =< s(98)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [46]: 21*s(106)+4*s(108)+2*s(118)+3*s(124)+12
Such that:s(122) =< V+V1
aux(38) =< 1
aux(39) =< V
aux(40) =< V1
s(108) =< aux(38)
s(118) =< aux(39)
s(106) =< aux(40)
s(124) =< s(122)
with precondition: [Out=1,V>=0,V1>=1]
* Chain [45]: 4*s(132)+1*s(133)+1*s(135)+12
Such that:s(133) =< 1
s(135) =< V1
aux(41) =< V
s(132) =< aux(41)
with precondition: [Out=1,V>=1,V1>=0]
* Chain [44]: 17*s(137)+5*s(139)+6*s(147)+3*s(156)+12
Such that:s(155) =< V+V1
aux(47) =< 1
aux(48) =< V
aux(49) =< V1
s(139) =< aux(47)
s(147) =< aux(48)
s(137) =< aux(49)
s(156) =< s(155)
with precondition: [V=Out+1,V>=2,V1>=0]
* Chain [43]: 135*s(163)+18*s(170)+18*s(173)+1*s(187)+12
Such that:s(187) =< V
aux(53) =< V1
s(163) =< aux(53)
s(169) =< aux(53)
s(170) =< s(163)*aux(53)
s(172) =< s(163)*s(169)
s(173) =< s(172)
with precondition: [V>=0,V1>=2,Out>=2]
* Chain [42]: 1*s(200)+3*s(201)+15*s(205)+27*s(206)+3*s(208)+3*s(209)+6*s(211)+12
Such that:s(200) =< V
s(203) =< V+V1
aux(54) =< V1
s(201) =< aux(54)
s(205) =< aux(54)
s(205) =< s(203)
s(206) =< s(203)
s(207) =< s(203)
s(208) =< s(206)*aux(54)
s(209) =< s(206)*s(203)
s(210) =< s(205)*s(207)
s(211) =< s(210)
with precondition: [V>=1,V1>=1,Out>=2]
* Chain [41]: 28*s(213)+15*s(216)+3*s(219)+3*s(220)+6*s(222)+1*s(223)+12
Such that:s(215) =< V1
aux(55) =< V
s(213) =< aux(55)
s(216) =< s(215)
s(216) =< aux(55)
s(218) =< aux(55)
s(219) =< s(213)*s(215)
s(220) =< s(213)*aux(55)
s(221) =< s(216)*s(218)
s(222) =< s(221)
s(223) =< s(215)
with precondition: [V>=2,V1>=0,Out>=2]
#### Cost of chains of start(V,V1,V9,V10,V19):
* Chain [57]: 2*s(224)+1*s(225)+215*s(227)+10*s(229)+10*s(234)+2*s(236)+2*s(237)+4*s(239)+54*s(243)+36*s(245)+10*s(250)+18*s(270)+18*s(272)+15*s(277)+3*s(280)+3*s(281)+6*s(283)+15*s(287)+3*s(289)+3*s(290)+6*s(292)+1*s(314)+12
Such that:s(225) =< V+1
s(314) =< V9
aux(57) =< 1
aux(58) =< -V+V1
aux(59) =< -V+V10
aux(60) =< V
aux(61) =< V+V1
aux(62) =< V1
aux(63) =< V10
s(250) =< aux(57)
s(229) =< aux(59)
s(243) =< aux(60)
s(227) =< aux(62)
s(224) =< aux(63)
s(245) =< aux(61)
s(229) =< aux(58)
s(234) =< aux(58)
s(235) =< aux(62)
s(236) =< s(234)*aux(63)
s(237) =< s(234)*aux(62)
s(238) =< s(229)*s(235)
s(239) =< s(238)
s(270) =< s(227)*aux(62)
s(271) =< s(227)*s(235)
s(272) =< s(271)
s(277) =< aux(62)
s(277) =< aux(61)
s(279) =< aux(61)
s(280) =< s(245)*aux(62)
s(281) =< s(245)*aux(61)
s(282) =< s(277)*s(279)
s(283) =< s(282)
s(287) =< aux(62)
s(287) =< aux(60)
s(288) =< aux(60)
s(289) =< s(243)*aux(62)
s(290) =< s(243)*aux(60)
s(291) =< s(287)*s(288)
s(292) =< s(291)
with precondition: [V>=0]
* Chain [56]: 2*s(316)+15*s(318)+5*s(319)+1*s(326)+1*s(327)+2*s(329)+8
Such that:aux(65) =< V10
aux(66) =< 1
aux(67) =< V1
s(316) =< aux(66)
s(318) =< aux(67)
s(319) =< aux(65)
s(319) =< aux(67)
s(325) =< aux(67)
s(326) =< s(318)*aux(65)
s(327) =< s(318)*aux(67)
s(328) =< s(319)*s(325)
s(329) =< s(328)
with precondition: [V=0,V9=0,V1>=0,V10>=1]
* Chain [55]: 2*s(333)+15*s(335)+5*s(336)+1*s(343)+1*s(344)+2*s(346)+8
Such that:aux(69) =< V10
aux(70) =< 1
aux(71) =< V1
s(333) =< aux(70)
s(335) =< aux(71)
s(336) =< aux(69)
s(336) =< aux(71)
s(342) =< aux(71)
s(343) =< s(335)*aux(69)
s(344) =< s(335)*aux(71)
s(345) =< s(336)*s(342)
s(346) =< s(345)
with precondition: [V=0,V1>=0,V9>=2,V10>=0]
* Chain [54]: 3*s(352)+40*s(353)+15*s(356)+3*s(359)+3*s(360)+6*s(362)+2*s(363)+12
Such that:aux(72) =< 1
aux(73) =< V1
aux(74) =< V10
s(352) =< aux(72)
s(363) =< aux(74)
s(353) =< aux(73)
s(356) =< aux(74)
s(356) =< aux(73)
s(358) =< aux(73)
s(359) =< s(353)*aux(74)
s(360) =< s(353)*aux(73)
s(361) =< s(356)*s(358)
s(362) =< s(361)
with precondition: [V=0,V1>=1]
* Chain [53]: 1*s(368)+19*s(370)+5*s(371)+1*s(378)+1*s(379)+2*s(381)+2*s(382)+1*s(383)+5*s(387)+5*s(392)+1*s(394)+1*s(395)+2*s(397)+6
Such that:s(368) =< 1
s(389) =< -V1+V9
s(387) =< -V1+V19
s(383) =< V1+1
aux(78) =< V9
aux(79) =< V19
s(382) =< aux(79)
s(370) =< aux(78)
s(387) =< s(389)
s(392) =< s(389)
s(377) =< aux(78)
s(394) =< s(392)*aux(79)
s(395) =< s(392)*aux(78)
s(396) =< s(387)*s(377)
s(397) =< s(396)
s(371) =< aux(79)
s(371) =< aux(78)
s(378) =< s(370)*aux(79)
s(379) =< s(370)*aux(78)
s(380) =< s(371)*s(377)
s(381) =< s(380)
with precondition: [V=1,V1>=0,V9>=0,V10>=0,V19>=0]
* Chain [52]: 1*s(398)+12*s(400)+5*s(401)+1*s(408)+1*s(409)+2*s(411)+6
Such that:s(398) =< 1
aux(81) =< V19
aux(82) =< V9
s(400) =< aux(82)
s(401) =< aux(81)
s(401) =< aux(82)
s(407) =< aux(82)
s(408) =< s(400)*aux(81)
s(409) =< s(400)*aux(82)
s(410) =< s(401)*s(407)
s(411) =< s(410)
with precondition: [V=1,V1=0,V9>=0,V10>=2,V19>=0]
* Chain [51]: 2*s(412)+1*s(413)+7*s(415)+5*s(417)+5*s(422)+1*s(424)+1*s(425)+2*s(427)+6
Such that:s(419) =< -V1+V9
s(417) =< -V1+V19
s(413) =< V1+1
s(418) =< V19
aux(83) =< V1
aux(84) =< V9
s(412) =< aux(83)
s(417) =< s(419)
s(415) =< aux(84)
s(422) =< s(419)
s(423) =< aux(84)
s(424) =< s(422)*s(418)
s(425) =< s(422)*aux(84)
s(426) =< s(417)*s(423)
s(427) =< s(426)
with precondition: [V=1,V10=0,V1>=1,V9>=0,V19>=V1+1]
* Chain [50]: 1
with precondition: [V=2,V1>=0,V9>=0,V10>=0,V19>=0]
* Chain [49]: 2*s(428)+1*s(429)+7*s(431)+5*s(433)+5*s(438)+1*s(440)+1*s(441)+2*s(443)+5
Such that:s(435) =< -V+V1
s(433) =< -V+V10
s(429) =< V+1
s(434) =< V10
aux(85) =< V
aux(86) =< V1
s(428) =< aux(85)
s(433) =< s(435)
s(431) =< aux(86)
s(438) =< s(435)
s(439) =< aux(86)
s(440) =< s(438)*s(434)
s(441) =< s(438)*aux(86)
s(442) =< s(433)*s(439)
s(443) =< s(442)
with precondition: [V9=0,V>=1,V1>=0,V10>=V+1]
Closed-form bounds of start(V,V1,V9,V10,V19):
-------------------------------------
* Chain [57] with precondition: [V>=0]
- Upper bound: 54*V+22+3*V*V+6*V*nat(V1)+nat(V1)*245+nat(V1)*3*V+nat(V1)*36*nat(V1)+nat(V1)*3*nat(V+V1)+nat(V1)*2*nat(-V+V1)+nat(V1)*4*nat(-V+V10)+nat(V9)+nat(V10)*2+nat(V10)*2*nat(-V+V1)+nat(V+V1)*36+nat(V+V1)*6*nat(V1)+nat(V+V1)*3*nat(V+V1)+ (V+1)+nat(-V+V1)*10+nat(-V+V10)*10
- Complexity: n^2
* Chain [56] with precondition: [V=0,V9=0,V1>=0,V10>=1]
- Upper bound: 15*V1+10+V1*V1+2*V1*V10+5*V10+V10*V1
- Complexity: n^2
* Chain [55] with precondition: [V=0,V1>=0,V9>=2,V10>=0]
- Upper bound: 15*V1+10+V1*V1+2*V1*V10+5*V10+V10*V1
- Complexity: n^2
* Chain [54] with precondition: [V=0,V1>=1]
- Upper bound: 40*V1+15+3*V1*V1+6*V1*nat(V10)+nat(V10)*17+nat(V10)*3*V1
- Complexity: n^2
* Chain [53] with precondition: [V=1,V1>=0,V9>=0,V10>=0,V19>=0]
- Upper bound: 19*V9+7+V9*V9+2*V9*V19+nat(-V1+V9)*V9+7*V19+V19*V9+nat(-V1+V9)*V19+ (V1+1)+nat(-V1+V9)*5+nat(-V1+V19)*5+nat(-V1+V19)*2*V9
- Complexity: n^2
* Chain [52] with precondition: [V=1,V1=0,V9>=0,V10>=2,V19>=0]
- Upper bound: 12*V9+7+V9*V9+2*V9*V19+5*V19+V19*V9
- Complexity: n^2
* Chain [51] with precondition: [V=1,V10=0,V1>=1,V9>=0,V19>=V1+1]
- Upper bound: 2*V1+7*V9+6+nat(-V1+V9)*V9+nat(-V1+V9)*V19+ (V1+1)+nat(-V1+V9)*5+ (-5*V1+5*V19)+ (-2*V1+2*V19)*V9
- Complexity: n^2
* Chain [50] with precondition: [V=2,V1>=0,V9>=0,V10>=0,V19>=0]
- Upper bound: 1
- Complexity: constant
* Chain [49] with precondition: [V9=0,V>=1,V1>=0,V10>=V+1]
- Upper bound: 2*V+7*V1+5+nat(-V+V1)*V1+nat(-V+V1)*V10+ (V+1)+nat(-V+V1)*5+ (-5*V+5*V10)+ (-2*V+2*V10)*V1
- Complexity: n^2
### Maximum cost of start(V,V1,V9,V10,V19): max([nat(V1)*2+4+max([nat(V1)*5+max([nat(V1)*8+5+nat(V1)*nat(V1)+nat(V10)*2+max([nat(V1)*2*nat(V10)+nat(V10)*3+nat(V10)*nat(V1),nat(V1)*25+5+nat(V1)*2*nat(V1)+max([nat(V1)*6*nat(V10)+nat(V10)*15+nat(V10)*3*nat(V1),54*V+7+3*V*V+6*V*nat(V1)+nat(V1)*205+nat(V1)*3*V+nat(V1)*33*nat(V1)+nat(V1)*3*nat(V+V1)+nat(V1)*2*nat(-V+V1)+nat(V1)*4*nat(-V+V10)+nat(V9)+nat(V10)*2*nat(-V+V1)+nat(V+V1)*36+nat(V+V1)*6*nat(V1)+nat(V+V1)*3*nat(V+V1)+ (V+1)+nat(-V+V1)*10+nat(-V+V10)*10])]),nat(-V+V1)*nat(V1)+2*V+nat(-V+V1)*nat(V10)+ (V+1)+nat(-V+V1)*5+nat(-V+V10)*5+nat(-V+V10)*2*nat(V1)]),nat(V9)*7+1+nat(-V1+V9)*nat(V9)+nat(-V1+V9)*nat(V19)+nat(V1+1)+nat(-V1+V9)*5+nat(-V1+V19)*5+nat(-V1+V19)*2*nat(V9)]),nat(-V1+V9)*nat(V9)+nat(V9)*7+nat(V19)*2+nat(-V1+V9)*nat(V19)+nat(V1+1)+nat(-V1+V9)*5+nat(-V1+V19)*5+nat(-V1+V19)*2*nat(V9)+ (nat(V9)*12+6+nat(V9)*nat(V9)+nat(V9)*2*nat(V19)+nat(V19)*5+nat(V19)*nat(V9))])+1
Asymptotic class: n^2
* Total analysis performed in 1226 ms.